$\forall$$A$, $V$:Type, $f$:$a$:$A$ fp$\rightarrow$ :$V$ $\times$ Top, ${\it eq}$:EqDecider($A$), $x$:$A$.
\\[0ex]($\uparrow$$x$ $\in$ dom($f$)) $\Leftarrow\!\Rightarrow$ ($x$ $\in$ fpf{-}domain($f$))